package ch.epfl.lara.matcheck.verify.axioms;

import ch.epfl.lara.matcheck.ast._
import ch.epfl.lara.matcheck.util.FreshName

trait ClassAxioms extends IAxiom 
                  with    PropositionalFormulaMaker
{ 
  import ifc._
  import Constants.SEP
  
  private var _subtyping   : Axiom = _
  private var _partitioning: Axiom = _
  private var _fields      : Axiom = _
  
  protected def classesAxioms(classes: List[ClassDef]) {
      _subtyping = conjunction(subtyping(classes)) 
      _partitioning = conjunction(partitioning(classes))
      _fields = conjunction(fieldAxioms(classes)) 
  }
  
  
  
  /**
   * <p>
   *        The subtyping relation over classes is mapped to its isomorphic set representation.
   *        If class B it's a subtype of C, then B <: C (where <: means subseteq).
   * </p>
   *
   * @return : A list of formulae. Each formula is of the forma B <: C if B is a subclass
   *               of C. 
   */ 
  private def subtyping(classes: List[ClassDef]): Axioms = 
    for(klass <- classes if klass.superclass.isDefined) yield {      
      // 1. Subtyping relation is converted to subset inclusion
      SubsetEq(Set(klass.getName),Set(klass.superclass.get))
    }
   
    
  private def partitioning(classes: List[ClassDef]): Axioms = {
    val (abstrclss,concreteclss) = (classes).partition(_.isAbstract)
    for(abstr <- abstrclss) yield {
      classes.filter(klass => klass.superclass.isDefined && 
                             klass.superclass.get == abstr.getName)
                            .map(klass => Set(klass.getName)) match {
        case Nil => Tru
         
        case children =>
          val length = children.length
          val fresh = FreshName.fresh("klass")
          val complete = if(abstr.isSealed) 
                           Forall(fresh,Imply(In(fresh,Set(abstr.getName)),disjunction(children.map(In(fresh,_)))))
                         else
                           Tru
          val disjoint = Forall(fresh,Imply(In(fresh,Set(abstr.getName)),
              conjunction(for(i<-List.range(0,length);j<-List.range(i+1,length)) yield {
                Neg(And(In(fresh,children(i)),In(fresh,children(j))))
              })
          ))
          And(complete,disjoint)
       }
     }
  }
  
  
  private def fieldAxioms(classes: List[ClassDef]): Axioms = 
    for(klass<-classes if !klass.isAbstract) yield {
      val fresh = FreshName.fresh("field")
      Forall(fresh, Imply(In(fresh,Set(klass.getName)),
        conjunction(
          for(FieldDef(name,tpe)<-klass.fields) yield {    
            In(Function(klass.getName+SEP+"getField"+SEP+name.getName,List(fresh)),Set(tpe.toString))
          }
        ))
      )
    }
  
  def subtyping   : Axiom = _subtyping
  def partitioning: Axiom = _partitioning
  def fields      : Axiom = _fields
  
  def classes     : Axiom = conjunction(subtyping :: partitioning :: fields :: Nil)
}
